Nuprl Definition : qadd_grp
11,40
postcript
pdf
qadd_grp == <rationals,
x
,
y
. qeq(
x
;
y
),
x
,
y
. q_le(
x
;
y
),
x
,
y
.
x
+
y
, 0,
x
.-(
x
)>
latex
clarification:
qadd_grp == <rationals,
x
,
y
. qeq(
x
;
y
),
x
,
y
. q_le(
x
;
y
),
x
,
y
.
x
+
y
, 0,
x
.(-1) *
x
>
latex
Definitions
rationals
,
qeq(
r
;
s
)
,
q_le(
r
;
s
)
,
r
+
s
,
<
a
,
b
>
,
x
.
A
(
x
)
,
r
*
s
,
-
n
,
#$n
FDL editor aliases
qadd_grp
origin